Inference at * 
Iof proof for Lemma do-apply-compose:


  A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)), x:A.
  (can-apply(f o g  ;x))  (do-apply(f o g  ;x) ~ do-apply(f;do-apply(g;x))) 

latex

 by ((UnivCD) 
CollapseTHENA (Auto)) 
CollapseTHEN ((MoveToConcl (-1)) 
CollapseTHEN ((
CRepUR ``do-apply can-apply p-compose`` ( 0)) 
CollapseTHEN (((GenConclAtAddr [1;1;1;1;1]) 

CoCollapseTHENA (Auto)) 
CollapseTHEN ((D (-2)) 
CollapseTHEN ((Reduce 0) 
CollapseTHEN (Auto
C)))))) 

latex

C.

Definitions

Type, f o g  , can-apply(f;x), do-apply(f;x), f(a), Top, s = t, x:A. B(x), x:AB(x), t  T, left + right, b, P  Q, False